$\forall$$T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$a$, $b$:$T$. Dec($R$($a$,$b$)))
\\[0ex]$\Rightarrow$ (connex($T$;$R$) $\Leftarrow\!\Rightarrow$ \{$\forall$$a$, $b$:$T$. (($R$$\backslash$)($a$,$b$)) $\vee$ (($R$$\rightleftharpoons$)($a$,$b$)) $\vee$ (($R$$\backslash$)($b$,$a$))\})